Ecosystem abstraction (for Solana support) by ericeil · Pull Request #96 · Certora/AutoProver

ericeil · 2026-07-23T18:42:34Z

PR 1 of 3 — Ecosystem abstraction (EVM + Solana front-half)

Part of the stacked split of the Crucible work (and preparatory for full Solana Prover support).
Stack: master → eric/ecosystem → eric/rust → eric/crucible-app.

Introduces a runtime ecosystem seam so the shared pipeline driver generalizes over the
analyzed domain instead of being hard-wired to Solidity — and lands the Solana front half
(analysis + property extraction) against it. EVM behavior is unchanged (the driver defaults
to ecosystem=EVM); Solana is added as a second ecosystem, exercised end-to-end by a null
(no-verifier) backend. The Solana verification backend (Crucible) is PR 3.

The seam

composer/pipeline/ecosystem.py (new) — Ecosystem[App, Main, Unit] + Language frozen
dataclasses, the EVM / SOLANA bindings, and the ECOSYSTEMS registry. An ecosystem factors
into a language facet (how the analyzed source is read — Solidity vs Rust) and a chain facet
(model + prompts + unit split).
composer/pipeline/core.py — run_pipeline takes an ecosystem (default EVM) and drives
the front half through it (analyzed-model type, prompts, validation, locate_main, units).
The per-unit loop iterates ecosystem.units(main) over any FeatureUnit.
composer/spec/system_model.py — the ecosystem-agnostic FeatureUnit protocol; EVM stays
bound to ContractInstance / ContractComponentInstance with byte-identical cache keys.
prop_inference.py / system_analysis.py / cli.py / ptypes.py — threaded through to
accept the ecosystem's prompts/units/Main generics.

Typing

PreparedSystem.main and the PipelineBackend[..., U, Main] generics carry Main/FeatureUnit
instead of Any; _batch_cache_key is typed via a result-type witness.
The one deliberately-erased boundary (run_pipeline's ecosystem: Ecosystem[Any, Any, Any]) is
documented with the invariance reasoning.
FeatureUnit.context_tag / feature_json return dict[str, object]; dropped a no-op
@runtime_checkable.

Solana front half

composer/spec/solana/model.py (new) — SolanaApplication (the standalone analog of
SourceApplication): programs, instructions, account constraints, CPIs, signers; plus the
SolanaProgramInstance / SolanaInstructionInstance index wrappers. Whole-program extraction
(units → a singleton [program]).
composer/spec/solana/null_backend.py (new) — a report-only backend that records extracted
properties without verifying, so the front half can be gated without a prover.
composer/templates/solana/* — Solana analysis + property prompts, and the RUST language's
rust/_failure_modes.j2 fragment they compose in.

Shared prompt partials (EVM + Solana dedup)

The EVM and Solana prompts duplicated a lot of mechanical boilerplate (the iterative prior-rounds
block, quality-over-quantity / adaptive-thinking guidance, the architect Behavior/Tools block, the
analysis memory paragraph) — and the copies had drifted. Factored into
composer/templates/shared/* carrying the EVM canonical wording, with the one domain noun
(component/program) parameterized. Mechanical boilerplate unified; domain prose (backgrounds,
examples, failure modes) left per-file. EVM prompts render byte-identical; Solana re-converges
to canonical wording.

Docs & tests

ARCHITECTURE.md (new) — high-level system map, written around the ecosystem seam.
docs/ecosystem-abstraction.md — describes the implemented seam (present tense).
tests/test_null_solana_backend.py (new) — deterministic unit test of the null backend
(no LLM / Postgres / prover).
CLAUDE.md — repo rule against from __future__ import annotations.

(The Rust application framework doc application-abstraction.md lives with PR 3, where that code
lands.)

🤖 Generated with Claude Code

Runtime Ecosystem/Language seam; the pipeline driver generalized over FeatureUnit/Main; EVM reproduces today's behavior exactly; Solana added as a second ecosystem (analysis + property extraction) proven against a null (no-verifier) backend. Built on origin/master (which already carries the command sandbox, #73). Stacked-PR 1 of 3 (eric/ecosystem -> eric/rust -> eric/crucible-app); see docs/pr-split-plan.md. Squashed from eric/crucible's final file state for this layer. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The located "main" was `Any`. It is a distinct axis from `FeatureUnit` — the per-unit protocol the extraction phase iterates — and EVM's main (`ContractInstance`) is not a FeatureUnit at all, so it can't just be typed as one. It IS the `Main` type the ecosystem seam already carries (`Ecosystem[App, Main, Unit]`). Thread that `Main` through: `PreparedSystem[FormT, U, Main]` (main: Main), `PipelineBackend[..., U, Main]` (prepare_system -> PreparedSystem[FormT, U, Main]), and `run_pipeline`. Each backend now binds it concretely — EVM foundry/prover to `ContractInstance`, the Solana null backend to `SolanaProgramInstance`. The internal `_extract_all` keeps `main: Any` on purpose: it drives the type-erased `Ecosystem[Any, Any, Any]`, so there is nothing to tie it to there. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

_batch_cache_key returned CacheKey[ComponentGroup, Any] because its value type isn't inferable from `props`, CacheKey/WorkflowContext are invariant (so the BackendResult bound won't assign to the caller's WorkflowContext[FormT]), and a return-only TypeVar trips reportInvalidTypeVarUse. Thread the concrete result type as a witness argument (`result_type: type[FormT]`, passed as the formalizer's `formalized_type` already in scope at the sole core-owned call site). FormT is now inferred from an argument, so the batch cache key is typed to exactly the backend's result — no Any, no warning. Pure typing change; the key value (props hash) is unchanged. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The `ecosystem: Ecosystem[Any, Any, Any]` param reads like an accidental weakening; it isn't. Ecosystem is invariant, the backend (and its Main) is a free var at this generic boundary so a concrete EVM/SOLANA argument can't unify with a tied param, prepare_system fixes analyzed: SourceApplication, and the backend's U isn't the ecosystem's Unit — so App/Main/Unit can't be tied without a protocol refactor, and the pairing is a runtime contract. Comment only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The only global_extraction ecosystem (SOLANA) sets collapse_units=True, so the per-property fan-out branch — Ecosystem.property_unit, _solana_property_unit, and the `else` limb in _extract_all — was never reached. It was the prototype that finding-level attribution superseded. Remove it: global extraction now always collapses to one whole-program batch (asserted). Also drops the now-unused SolanaInvariantUnit / PropertyFormulation imports. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…leans After removing the per-property fan-out, global_extraction and collapse_units each carried the same single bit as `extraction_unit is not None`, and Solana's required `units` (_solana_units) was dead (never called in whole-program mode). Collapse the three signals into one invariant: an ecosystem sets exactly one of `units` (per-component) xor `extraction_unit` (whole-program), and _extract_all branches on which is present. Both callables are now Optional; drop global_extraction, collapse_units, and _solana_units; type SOLANA's Unit param as SolanaProgramInstance (the whole-program unit) and drop the now-unused SolanaInstructionInstance import. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

extraction_unit was equivalent to units() returning a single unit: both feed the same per-unit _extract (same cache context, task, prompts, empty-props drop). It was only distinct as a vestige of the removed fan-out. Collapse it: units is required again and returns a list; Solana returns a singleton [main] (its whole program is the one unit), EVM one per component. _extract_all is now a single gather over ecosystem.units(main) — structurally master's _one loop again, minus the ecosystem-generic bits (units(main), feat.context_tag(), ecosystem prompts). Pyright (CI paths) clean; EVM pipeline/foundry tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

FeatureUnit has no isinstance/issubclass call sites, so @runtime_checkable (and its import) bought nothing. Type context_tag()/feature_json() as dict[str, object] across the protocol and every impl (ContractComponentInstance, Solana program/invariant/ instruction units) — all return str-keyed, JSON-able dicts, and the sole consumer (WorkflowContext.child(tag)) accepts it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The doc shipped in the ecosystem-abstraction commit but still described the pre-ecosystem, Solidity-only, per-component world. Update it to match: - §1/§2: reframe as smart-contract (not Solidity-only) and call out the ecosystem front-half as a second, backend-orthogonal axis of pluggability. - §3/§4: per-component -> per-unit (units() / FeatureUnit); correct the backend signature to PipelineBackend[P, FormT, H, A, U, Main] and PreparedSystem holding Main; add a new "ecosystem seam" subsection. - §4 step 1: analyzed model type is set by the ecosystem, not the backend. - §10: add the Solana front-half (model + prompts + whole-program units). Also drop the now-dangling extraction_unit reference in core.py's PreparedSystem.main comment (removed in the units() unification). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

… fragment ecosystem-abstraction.md was a proposal (title, "Status: proposal", phased plan, open questions, future tense) and had drifted from the code. Rewrite it as present-tense documentation of the implemented seam: - Describe the actual Language + Ecosystem dataclasses and the ECOSYSTEMS registry (not the earlier Language+Chain protocol sketch). - Cover only what exists: the seam, EVM (SOLIDITY ⊕ evm), and the Solana front half (RUST ⊕ solana, whole-program units, shared Rust fragment). - Drop the unbuilt/off-branch material (Soroban chain, verification backends, rustapp selection wiring) and the dead companion links. - Refresh the ecosystem.py module docstring to match. Also fix a real PR-split bug this surfaced: solana/property_prompt.j2 does `{% include "rust/_failure_modes.j2" %}` and RUST.failure_modes_partial points at it, but the file was only added on the PR2 (rust) branch — so rendering the Solana property prompt raised TemplateNotFound on this branch. Add the file here, alongside the Solana front half that consumes it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

application-abstraction.md documents the (Rust) application framework, which belongs with the crucible-app PR, not this front-half ecosystem PR. Remove it here and drop the now-dangling companion link from ecosystem-abstraction.md; it is re-added on eric/crucible-app. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Pin the rendered text of the EVM + Solana analysis/property prompts so that factoring shared boilerplate into partials is provably behaviour-preserving. Renders each template with a permissive context stub (dynamic per-target bits blank out; static boilerplate renders in full) across two control-flow variants (existing-source + prior rounds, greenfield + none). Baseline captured from the current templates; EVM goldens must not change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The EVM and Solana analysis/property prompts duplicated a lot of mechanical boilerplate (the iterative prior-rounds block, the quality-over-quantity and adaptive-thinking guidance, the architect Behavior/Tools block, the analysis memory-tool paragraph) — and the copies had already drifted in wording. Extract that boilerplate into composer/templates/shared/*, carrying the EVM canonical wording, with the one domain noun ("component"/"program") parameterized via a `unit_noun` with-scope. Both ecosystems now `{% include %}` the partials. Domain-specific prose (backgrounds, category examples, failure modes, the Rust-source paragraph, the "Reasoning is load-bearing" example) stays per-file — mechanical boilerplate unified aggressively, prose left alone. EVM goldens are byte-identical (verified). Solana re-converges to the canonical wording (goldens updated); nouns stay correct ("program", not "component"). Net: -135 lines across the 8 templates. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The golden snapshot test served as a one-time guard rail to verify the shared-partial prompt refactor was behaviour-preserving (EVM byte-identical). Its job is done and we don't want the goldens/test carried into master, so remove the test module and its snapshot fixtures. The shared/ prompt partials themselves stay. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The null backend (composer/spec/solana/null_backend.py) had no focused coverage — only the expensive live-LLM gate (tests/test_solana_gate.py, on the rust/crucible branches) used it incidentally. Add a deterministic unit test (no LLM / Postgres / prover) on the branch that introduces the backend: formalize echoes properties into a NullResult, fetch_verdicts is empty, prepare_system routes through SOLANA.locate_main and yields the formalizer, to_artifact_id derives the slugged filename, and the backend declares the Solana front-half phases/keys. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

julian-certora · 2026-07-27T21:22:16Z

+# Background
+
+{% if sort == "greenfield" %}
+You have been provided a system/design document describing a Solana application. No


Perhaps I am wrong, but it seems like a variable capturing the language, rather than the word Solana, might make prompts like this reusable for Soroban too...

julian-certora · 2026-07-27T21:25:33Z

similarly, files like .../composer/templates/analyzer_system_prompt.j2 that hardwire Solidity might be amenable to addiing a language variable and then perhaps be reusable?

jtoman · 2026-07-27T22:10:55Z

+    def context_tag(self) -> dict[str, object]:
+        """The tag persisted alongside this unit's workflow context."""
+        ...


you almost certainly want str, Any to mean, well, "any type".

jtoman · 2026-07-27T22:14:05Z

+    This is emphatically **not** the language the AutoProver backend is *implemented* in: a
+    backend implemented as a Rust wheel (:mod:`composer.rustapp`) may analyze Solidity
+    (``echoprover`` → EVM) or Rust (Crucible → Solana). The implementation language is not
+    associated with the ecosystem; only the analyzed-source language is.


uh.... duh? idk if we need this.

jtoman · 2026-07-27T22:15:45Z

+    #: Enumerate the units the extraction phase infers properties for — one batch per unit. EVM
+    #: returns one per component; a whole-program ecosystem (Solana) returns a singleton ``[main]``,
+    #: so all its invariants are inferred + formalized in a single harness + run
+    #: (docs/crucible-unit-granularity.md §3).


ref not found

jtoman · 2026-07-27T22:16:18Z

+    #: Typed over ``BaseApplication`` (not ``App``): the validator receives the produced model
+    #: and narrows internally (as ``_validate_connectivity`` does), and this keeps it assignable
+    #: to ``run_component_analysis``'s ``validate`` parameter without a contravariance clash.
+    validate_analysis: Callable[[BaseApplication, SolidityIdentifier | None], str | None]


"SolidityIdentifier"

jtoman · 2026-07-27T22:16:46Z

+class PromptPair:
+    """A (system prompt, initial prompt) template-name pair for one agent."""
+
+    system: str


are these the prompt wholesale? or the j2 name? If the latter, I'd much prefer these were typedtemplate instances.

jtoman · 2026-07-27T22:41:54Z

+{% else %}
+You have been provided a system/design document describing a Solana application, plus access to
+the Rust source (native and/or Anchor) that implements it.
+{% endif %}


I'm fairly certain I wrote a wrapper that gracefully handles the case where the system doc is None. I'd urge you to adapt and then use that.

jtoman · 2026-07-27T22:48:37Z

+#### Instructions
+
+Each instruction (the program's entry points / handlers). For each:
+
+- `name`: the instruction's snake_case name.
+- `description`: what it does behaviorally (not how).
+- `args`: its non-account arguments (name & type).
+- `accounts`: every account it takes in its accounts context. For each account give its `name`,
+  its `account_type` (e.g. `Signer`, `Account<Vault>`, `Program`, `SystemAccount`,
+  `UncheckedAccount`, a PDA of specific seeds), its `roles` (signer / writable / readonly / pda /
+  program / sysvar), and the `constraints` the program is responsible for enforcing on it
+  (signer/owner checks, `has_one`, `seeds`+`bump`, `address`, or documented invariants). If an
+  account has no enforced constraints, record an empty list — that is itself important signal.
+- `signers`: which accounts must sign (the authorities the instruction authenticates).
+- `cpis`: cross-program invocations it performs (target program + what it does / signer used).
+- `requirements`: the instruction's behavioral specification, stated as requirements ("The
+  instruction must ...").


wait hang on. Are you SURE you want this level of granularity?

The Solidity pipeline pretty intentionally chose the (rather vague) notion of "Component" to sit between "a single entry point" and "the whole ass contract". If there are, say, 20 entry points that means we'll get 20 property inference passes, 20 CVLR authors etc. Further I think (but can't prove) that thinking about functional units, not individual entry points is the more useful framing for properties.

I'm curious why you chose Instructions (~ entry points) specifically over the same abstract notion of "component" from the solidity world. I'm perfectly open to being told the abstraction doesn't transplant cleanly to Solana smart contracts.

jtoman · 2026-07-27T22:49:41Z

+{% set siblings = [] %}
+{% for p in context.app.programs %}{% if p.program_identifier != context.program.program_identifier %}{% set _ = siblings.append(p) %}{% endif %}{% endfor %}


what the. Just make this a computed property of whatever p is?

jtoman · 2026-07-27T22:50:27Z

+The program owns / derives these account (state) types: {{ context.program.account_types | join(", ") }}.
+{% endif %}
+
+The program exposes these instructions (the actions a fuzzer will drive in random sequences):


strange choice to "hardcode" fuzzer here. There must be some backend agnostic verbiage we can use.

jtoman · 2026-07-27T22:51:26Z

+## Step 1
+
+Analyze the provided {% if sort != "greenfield" %}implementation{% else %}design{% endif %} and formulate a set of security
+properties that are PLAUSIBLE for this program. Prefer **cross-instruction** properties — ones a


but isn't this whole pass explicitly scoped to a single instruction? that's what seems weird to me.

This was referenced Jul 23, 2026

PR 2/3: Rust application framework (PyO3) #97

Draft

PR 3/3: Crucible backend (capstone) #98

Draft

ericeil force-pushed the eric/ecosystem branch 2 times, most recently from 4c76f66 to 833557a Compare July 23, 2026 19:58

ericeil force-pushed the eric/ecosystem branch from 833557a to fe84bae Compare July 23, 2026 20:15

ericeil and others added 16 commits July 23, 2026 13:59

Remove unneeded comment

5c61dbd

Comment tweaks

7d36604

Comment tweaks

29c2a9f

tweaks

530ed48

ericeil changed the title ~~PR 1/3: Ecosystem abstraction (EVM + Solana front-half)~~ Ecosystem abstraction (Part 1 of Solana support) Jul 23, 2026

ericeil changed the title ~~Ecosystem abstraction (Part 1 of Solana support)~~ Ecosystem abstraction (for Solana support) Jul 23, 2026

ericeil and others added 2 commits July 23, 2026 17:01

ericeil marked this pull request as ready for review July 24, 2026 00:15

ericeil requested review from jtoman and julian-certora July 24, 2026 00:15

julian-certora reviewed Jul 27, 2026

View reviewed changes

jtoman requested changes Jul 27, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Ecosystem abstraction (for Solana support) - #96

Ecosystem abstraction (for Solana support)#96
ericeil wants to merge 19 commits into
masterfrom
eric/ecosystem

ericeil commented Jul 23, 2026 •

edited

Loading

Uh oh!

julian-certora Jul 27, 2026

Uh oh!

julian-certora commented Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

jtoman Jul 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		{% set siblings = [] %}
		{% for p in context.app.programs %}{% if p.program_identifier != context.program.program_identifier %}{% set _ = siblings.append(p) %}{% endif %}{% endfor %}

Uh oh!

Conversation

ericeil commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR 1 of 3 — Ecosystem abstraction (EVM + Solana front-half)

The seam

Typing

Solana front half

Shared prompt partials (EVM + Solana dedup)

Docs & tests

Uh oh!

Choose a reason for hiding this comment

Uh oh!

julian-certora commented Jul 27, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ericeil commented Jul 23, 2026 •

edited

Loading